(declare-fun a () (Seq Int))
(declare-fun b () (Seq Int))
(declare-fun c () (Seq Int))
(declare-fun x () Int)
(declare-fun y () Int)
(assert (or (= b c) (= a c)))
(assert (= (seq.nth c 0) (seq.nth c x)))
(assert (not (= (seq.nth b y) (seq.nth c y))))
(check-sat)
